eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
IFRM(false, N, add(M, X)) → RM(N, X)
PURGE(add(N, X)) → PURGE(rm(N, X))
EQ(s(X), s(Y)) → EQ(X, Y)
RM(N, add(M, X)) → EQ(N, M)
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
PURGE(add(N, X)) → RM(N, X)
IFRM(true, N, add(M, X)) → RM(N, X)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IFRM(false, N, add(M, X)) → RM(N, X)
PURGE(add(N, X)) → PURGE(rm(N, X))
EQ(s(X), s(Y)) → EQ(X, Y)
RM(N, add(M, X)) → EQ(N, M)
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
PURGE(add(N, X)) → RM(N, X)
IFRM(true, N, add(M, X)) → RM(N, X)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQ(s(X), s(Y)) → EQ(X, Y)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQ(s(X), s(Y)) → EQ(X, Y)
The value of delta used in the strict ordering is 3.
POL(EQ(x1, x2)) = (3)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
IFRM(false, N, add(M, X)) → RM(N, X)
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
IFRM(true, N, add(M, X)) → RM(N, X)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFRM(false, N, add(M, X)) → RM(N, X)
IFRM(true, N, add(M, X)) → RM(N, X)
Used ordering: Polynomial interpretation [25,35]:
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
The value of delta used in the strict ordering is 12.
POL(add(x1, x2)) = 4 + x_1 + x_2
POL(RM(x1, x2)) = 4 + (4)x_2
POL(eq(x1, x2)) = 1
POL(true) = 0
POL(false) = 0
POL(s(x1)) = 3 + (3)x_1
POL(IFRM(x1, x2, x3)) = (4)x_1 + (4)x_3
POL(0) = 1
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
PURGE(add(N, X)) → PURGE(rm(N, X))
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PURGE(add(N, X)) → PURGE(rm(N, X))
The value of delta used in the strict ordering is 2.
POL(add(x1, x2)) = 1 + (2)x_2
POL(eq(x1, x2)) = 0
POL(true) = 3
POL(rm(x1, x2)) = x_2
POL(false) = 0
POL(s(x1)) = 2 + (3)x_1
POL(ifrm(x1, x2, x3)) = x_3
POL(0) = 1
POL(nil) = 0
POL(PURGE(x1)) = (2)x_1
rm(N, nil) → nil
ifrm(true, N, add(M, X)) → rm(N, X)
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))